FDL - Nuprl Definition : antecedent-surjection

Nuprl Definition : antecedent-surjection

11,40

P == Q

P & (

e:{e:E| Q(e)} .

e':{e:E| P(e)} . (f(e') = e))

clarification:

antecedent-surjection(es;P;Q;f)
== antecedent-function(es;P;Q;f)
== & (

e:{e:es-E(es)| Q(e)} .

e':{e:es-E(es)| P(e)} . (f(e') = e

es-E(es)))

Definitions P & Q, Q f P, x:A. B(x), x:A. B(x), {x:A| B(x)} , s = t, E, f(a)

FDL editor aliases antecedent-surjection

Definitions	P & Q, Q f P, x:A. B(x), x:A. B(x), {x:A\| B(x)} , s = t, E, f(a)
FDL editor aliases	antecedent-surjection